| Definitions | t  T,  x:A. B(x), isrcv(e),  b, P  Q, Id, s = t, left+right, P   Q, valtype(e), Valtype(da;k), val(e), x:A B(x), P & Q, IdDeq, Type,  x.A(x),  x. t(x), x : v, f  g, {T}, P  Q, msg-spec-links(snd), IdLnkDeq, IdLnk, remove-repeats(eq;L), (x l), {x:A| B(x) }, ES, Top, f(x)?z, source(l), vartype(i;x), x:A  B(x), Void, kind(e), KindDeq, Knd, ecl-tags(l;snd), tag(e), lnk(e), E, A & B, loc(e), rcv(l,tg), type List, nil, EqDecider(T), Prop,  A, b,  , State(ds), ecl-m3(a;snd;x;l), S  T, f(a), a:A fp B(a), Atom$n, msg-spec(ds;da), Normal(T), xdom(f). v=f(x) P(x;v), Normal(ds), Normal(da), xL. P(x), msg-spec-loc-decl(snd;i;da),  x:A. B(x), es-decls(es;i;ds;da), 1of(t), SQType(T), s ~ t, state@i, (state when e), tagged-list-messages(s;v;L), deq-member(eq;x;L), Unit, if b t else f fi, with decls ds dasends on l from e include f(e) and only these for tags in tgs, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val), AtomFree(T;x), R-lnk-tags(ds;da;l;tgs;ks;g), x,y. t(x;y), ecl-machine3(ds;da;x;T;ks;a;snd),  , lnk(k), destination(l), isrcv(k), x dom(f), R ||- es.P(es), ||as||, False, A B,  , 2of(t), map(f;as), product-deq(A;B;a;b), fpf-vals(eq;P;f), l-union-list(eq;ll), a<b, no_repeats(T;l), msg-item(ds;da;k;l),  x:A. B(x), <a,b>, P Q, f(x), Dec(P), reduce(f;k;as), Y, Case of a; nil s ; x.y, rec:z t(x;y;z), p q, Case b of inl(x) s(x) ; inr(y) t(y), eqof(d), A/x,y. B(x;y), union-deq(A;B;a;b), sumdeq(a;b), sum-deq(A;B;a;b), *, inr(x), proddeq(a;b), p  q, prod-deq(A;B;a;b), Atom2Deq, eq_atom$n(x;y), if a=1 b then x else y, atom2-deq-aux, inl(x), n+m, l[i], hd(l), nth_tl(n;as), ij, i<j, if a<b c ; d fi, n-m, tl(l), msg-spec-loc(snd;i), A || B |
| Lemmas | R-lnk-tags-compat2, R-compat wf, decidable equal IdLnk, msg-spec-loc-decl-implies, member-remove-repeats, decidable assert, nil member, fpf-ap wf, member map, member-ecl-tags, bool cases, bool sq, product-deq wf, msg-item wf, pi1 wf, pi2 wf, R-lnk-tags-rule, normal-ds-join, normal-ds-single, length wf1, l-union-list wf, Knd sq, no repeats-ecl-tags, fpf-dom wf, fpf-trivial-subtype-top, msg-spec-loc-decl wf, l all wf, isrcv wf, ldst wf, lnk wf, normal-da wf, normal-ds wf, normal-type wf, msg-spec wf, nat wf, fpf wf, R-all-rule, R-lnk-tags wf, es-decls wf, es-sends-iff wf, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, tagged-list-messages wf, es-state-when wf, subtype rel dep function, Id sq, ecl-m3 wf, decl-state wf, ma-valtype wf, bool wf, bnot wf, not wf, subtype rel self, deq wf, rcv wf, es-loc wf, es-E wf, es-lnk wf, es-tag wf, ecl-tags wf, es-valtype wf, Knd wf, Kind-deq wf, es-kind wf, es-vartype wf, lsrc wf, fpf-cap wf, top wf, event system wf, l member wf, remove-repeats wf, IdLnk wf, idlnk-deq wf, msg-spec-links wf, es-decls-iff, fpf-join wf, fpf-single wf, Id wf, id-deq wf, es-val wf, assert wf, es-isrcv wf |
a:(